Assertion-based verification (ABV) is a methodology utilized in hardware design verification, and is reflected in the standardization of some assertion languages. For example, PSL (Property Specification Language) was adopted as an Institute of Electrical and Electronics Engineers (IEEE) standard (IEEE standard 1850, “Standard for PSL: Property Specification Language”), and is used in electronic design automation (EDA) for formal verification as well as for simulation of complex hardware designs.
In formal verification, or model checking, an exhaustive analysis of the design state-space is performed in order to determine, across substantially all possible scenarios, whether the design obeys its specification.
For example, assertions written in PSL may be embedded in the register transfer level (RTL) description of a hardware design, and may then be formally verified through model checking. The behavioral specifications define intended design behavior, which is expected to be demonstrated during verification and further define error situations, which are expected to not occur during verification. Behavioral specifications may thus provide improved visibility into the internal state of a design.
Properties in a specification language may be classified into safety properties, which possess a finite counterexample; and liveness properties, which do not possess a finite counterexample. For example, a safety property states that a “bad” event never happens, for example, that “two processes are never at the critical section together”; whereas a liveness property states that a “good” event eventually happens, for example, that “Process A eventually enters the critical section.”
Verifying safety properties may be insufficient to assure that a design meets its requirements, since a safety property may pass even if nothing actually occurs in the design under test. A bounded safety property may be used to check that an event actually occurs, but may fail if the event occurs outside of the defined bound. Unfortunately, increasing the bound may result in an undesirably large automaton or in an inefficient model checking process. Additionally, the counterexample for a bounded property may be long and difficult to inspect.
In contrast, in cases where the exact cycle on which the event occurs is not important, a liveness property may provide a useful answer, and may result in a smaller automaton as well as an efficient model checking process (e.g., more efficient than the model checking process of a bounded property).